(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 119))
(declare-fun v2 () (_ BitVec 68))
(declare-fun a3 () (Array  (_ BitVec 54)  (_ BitVec 67)))
(declare-fun a4 () (Array  (_ BitVec 98)  (_ BitVec 27)))
(assert (let ((e5(_ bv2 5)))
(let ((e6 ((_ rotate_right 0) v0)))
(let ((e7 (concat v0 e6)))
(let ((e8 (ite (bvugt v2 ((_ sign_extend 60) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e9 (bvudiv ((_ sign_extend 67) e8) v2)))
(let ((e10 (ite (bvsle v1 ((_ zero_extend 111) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e11 (ite (= (_ bv1 1) ((_ extract 3 3) e5)) ((_ sign_extend 67) e8) e9)))
(let ((e12 (store a4 ((_ extract 112 15) v1) ((_ extract 26 0) v2))))
(let ((e13 (store a4 ((_ zero_extend 30) v2) ((_ zero_extend 26) e10))))
(let ((e14 (select e12 ((_ sign_extend 30) e9))))
(let ((e15 (store e13 ((_ zero_extend 90) e7) ((_ sign_extend 26) e10))))
(let ((e16 (select e12 ((_ sign_extend 30) e11))))
(let ((e17 (ite (bvult v0 ((_ sign_extend 3) e10)) (_ bv1 1) (_ bv0 1))))
(let ((e18 (ite (= (_ bv1 1) ((_ extract 1 1) e6)) ((_ zero_extend 26) e17) e16)))
(let ((e19 ((_ zero_extend 16) e16)))
(let ((e20 (bvmul ((_ sign_extend 76) e19) v1)))
(let ((e21 (ite (bvult e7 e7) (_ bv1 1) (_ bv0 1))))
(let ((e22 ((_ rotate_left 11) e14)))
(let ((e23 (bvnot e17)))
(let ((e24 (bvsub ((_ sign_extend 118) e8) e20)))
(let ((e25 (bvshl e11 ((_ sign_extend 67) e23))))
(let ((e26 ((_ rotate_left 21) e22)))
(let ((e27 ((_ zero_extend 58) v2)))
(let ((e28 (bvnand ((_ sign_extend 26) e17) e18)))
(let ((e29 ((_ rotate_right 58) e9)))
(let ((e30 (bvlshr ((_ sign_extend 22) e5) e18)))
(let ((e31 (bvsgt ((_ sign_extend 41) e22) e29)))
(let ((e32 (bvsle ((_ sign_extend 115) e6) e20)))
(let ((e33 (bvule ((_ zero_extend 92) e16) v1)))
(let ((e34 (bvult e19 ((_ zero_extend 42) e21))))
(let ((e35 (bvslt ((_ zero_extend 35) e7) e19)))
(let ((e36 (bvult ((_ sign_extend 63) e5) e29)))
(let ((e37 (bvslt v2 ((_ sign_extend 41) e28))))
(let ((e38 (bvuge ((_ sign_extend 67) e23) v2)))
(let ((e39 (bvuge e11 ((_ zero_extend 64) e6))))
(let ((e40 (bvule e25 ((_ zero_extend 41) e14))))
(let ((e41 (bvule e27 ((_ sign_extend 58) e9))))
(let ((e42 (bvuge ((_ zero_extend 92) e16) e20)))
(let ((e43 (distinct e9 ((_ zero_extend 41) e22))))
(let ((e44 (bvugt e24 ((_ sign_extend 118) e8))))
(let ((e45 (bvule e22 e28)))
(let ((e46 (bvslt v1 ((_ sign_extend 115) v0))))
(let ((e47 (bvsgt ((_ sign_extend 42) e17) e19)))
(let ((e48 (bvslt e6 ((_ sign_extend 3) e10))))
(let ((e49 (bvslt ((_ sign_extend 41) e18) e25)))
(let ((e50 (bvsgt e22 e16)))
(let ((e51 (bvsge ((_ zero_extend 114) e5) e24)))
(let ((e52 (bvsgt e19 ((_ sign_extend 42) e17))))
(let ((e53 (bvsge e14 ((_ sign_extend 19) e7))))
(let ((e54 (bvslt e9 ((_ sign_extend 41) e22))))
(let ((e55 (bvsle e9 ((_ zero_extend 63) e5))))
(let ((e56 (bvsge v2 ((_ zero_extend 67) e10))))
(let ((e57 (= ((_ zero_extend 41) e30) e29)))
(let ((e58 (bvsle e25 ((_ sign_extend 67) e23))))
(let ((e59 (bvuge e20 ((_ sign_extend 92) e14))))
(let ((e60 (bvugt e10 e8)))
(let ((e61 (bvsgt ((_ zero_extend 67) e10) e9)))
(let ((e62 (= e18 e28)))
(let ((e63 (= ((_ sign_extend 51) e29) e24)))
(let ((e64 (= e9 ((_ zero_extend 41) e26))))
(let ((e65 (ite e42 e53 e38)))
(let ((e66 (xor e39 e49)))
(let ((e67 (or e56 e32)))
(let ((e68 (ite e67 e33 e60)))
(let ((e69 (and e40 e65)))
(let ((e70 (and e35 e57)))
(let ((e71 (ite e46 e37 e70)))
(let ((e72 (xor e62 e58)))
(let ((e73 (xor e36 e69)))
(let ((e74 (= e66 e31)))
(let ((e75 (ite e44 e44 e71)))
(let ((e76 (and e75 e63)))
(let ((e77 (or e64 e72)))
(let ((e78 (and e43 e61)))
(let ((e79 (ite e51 e74 e45)))
(let ((e80 (not e78)))
(let ((e81 (not e52)))
(let ((e82 (and e48 e50)))
(let ((e83 (ite e41 e68 e34)))
(let ((e84 (=> e76 e54)))
(let ((e85 (=> e47 e55)))
(let ((e86 (and e80 e77)))
(let ((e87 (xor e73 e81)))
(let ((e88 (not e87)))
(let ((e89 (or e88 e79)))
(let ((e90 (= e86 e83)))
(let ((e91 (=> e59 e84)))
(let ((e92 (= e85 e89)))
(let ((e93 (or e91 e91)))
(let ((e94 (= e92 e93)))
(let ((e95 (and e90 e90)))
(let ((e96 (not e95)))
(let ((e97 (and e96 e94)))
(let ((e98 (= e82 e97)))
(let ((e99 (and e98 (not (= v2 (_ bv0 68))))))
e99
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
